In designing large dynamic systems such as, for example, a complex electronic circuit, the design is often analyzed to verify a selected property. For example, the design may need to be analyzed to verify that the system does not enter a certain state under any normal set of inputs to the system in any finite number of steps (e.g., a safety property).
One conventional approach is to use a bounded model checker that can verify whether the system will not enter a preselected state. For example, several Boolean satisfiability solvers (also referred to as SAT solvers) are known that can determine whether the system enters the state within a selected number of steps. Typically, the SAT solver searches for a counterexample (i.e., a set of inputs to the system that will cause the system to enter the preselected state within the selected number of steps). Thus, if the SAT solver finds a counterexample within K steps, the system can enter the preselected state. The designer can then redesign the system to ensure that the preselected state is not entered.
“However, even if the SAT solver cannot find a counterexample in K steps, there is still a chance that the system will enter the preselected state in greater than K steps. Thus, the design is only partially verified for the selected property. This “partial” verification is unacceptable in many applications.”
Another approach is to use an unbounded model checker that exhaustively calculates whether the system can enter the preselected state in any number of steps. However, this approach is only practical for relatively small systems because the number of states increases exponentially with the number of state variables (i.e., the so-called state explosion problem).
One modification of this approach is to use an abstraction of the design in the unbounded model checker. Subsequent abstractions are based on an analysis of the counterexample found in the previous iteration of the unbounded model checker. Typically, a constraint is introduced that prevents the counterexample from occurring. This approach tends to result in a relatively inefficient abstraction because the abstraction is an accumulation of the constraints introduced for each counterexample that was found in previous iterations. These added constraints may not be relevant to the preselected property, but there is no mechanism in this approach for removing an irrelevant constraint from the abstraction.